Add several negative properties of LRS_R deduced from those of Top#231
Add several negative properties of LRS_R deduced from those of Top#231dschepler wants to merge 4 commits into
Conversation
|
Thanks a lot! I am glad that we can finally decide some of the properties of this category. It's also good to see that you could generalize your proof that previously only worked for special ground rings. I have revised the content page, please check the three 3 commits that I added. I still need to check the proofs in |
| check_redundancy: false | ||
|
|
||
| - property: cartesian filtered colimits | ||
| proof: As a corollary of the results <a href="/content/LRS-not-cartesian-closed">here</a>, if we choose a quotient field $k$ of $R$, then the functor $\Top \to \LRS_R$ of equipping a topological space with the constant sheaf of $k$ is fully faithful, and preserves all colimits and all inhabited limits. Therefore, if $\LRS_R$ had cartesian filtered colimits, then $\Top$ would also, giving a contradiction. |
There was a problem hiding this comment.
I have some issues with this proof and the other ones (but no doubt that they are correct!). It is just said that "of the results here", but not making explicit which results are used for which claim. Also, I think that some of the proofs are even used. This suggests refactoring them.
Notice that for example the content page never mentions any functor from Top to LRSR where R is a commutative ring which is not a field.
Maybe it is even better to add all these proofs to the content page itself. It can be a huge corollary like "The category LRS_R is (a) not X, (b) not Y, ... ".
Notice that this "outsourcing" has already been done for the cartesian closed property. The current approach is inconsistent.
Also consider adding stuff to the page cartesian-closed-results.md that I created for the more general results. Probably it then should also be renamed, since it is not about ccc anymore, but rather about coreflections. Then it can also be merged with subobject_classifiers_coreflection.md, and also with exact_filtered_colimits_descend.md.
In a later stage of this project, all of this will part of an extended deduction system where properties of categories can be deduced automatically from properties and results of (adjoint) functors. Namely, functor implications will then also have fields like target_conclusions and left_adjoint_assumptions.
2 participants
Addresses: #227